Nuprl Lemma : onceR_feasible 11,40

i:Id. R-Feasible{i:l}(onceR{a:ut2, done:ut2}(i)) 
latex


Definitionsnormal-type{i:l}(T), A c B, False, A  B, Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), eq_atom{$n:n}(xy), atom2-deq, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), b, Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), t.2, t.1, (i = j), band(pq), R-interface-compat(AB), R-discrete_compat(AB), R-frame-compat(AB), R-base-domain(R), eq_bd(pq), Rda(R), Rds(R), R-loc(R), eq_id(ab), True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), P  Q, Rplus?(x1), i <z j, tl(l), i j, nth_tl(n;as), hd(l), prop{i:l}, guard(T), sq_type(T), A, lelt(ijk), Y, l[i], ||as||, int_seg(ij), decl-type{i:l}(dsx), Knd, eqof(d), if b then t else f fi , top, id-deq, xt(x), t  T, l_all(LTx.P(x)), R-compat{i:l}(AB), pairwise(x,y.P(x;y); L), P  Q, es_realizer{i:l}, tt, ff, es-state-ap(sx), b, mkid{$x:ut2}, onceR{$a:ut2, $done:ut2}(i), R-Feasible{i:l}(R), x:AB(x), , x:AB(x), P  Q, Unit, (x  l), P  Q, decidable(P), x(s), decl-state(ds), ,
Lemmasfinite-prob-space wf, decl-state wf, fpf wf, unit wf, l member wf, R-Feasible wf, false wf, natural number wf p-outcome, bool-inhabited, normal-ds-single, le wf, IdLnk wf, select member, fpf-empty wf, fpf-empty-compatible-left, fpf-single wf3, Knd wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, top wf, Kind-deq wf, fpf-empty-compatible-right, fpf-compatible-self, assert-eq-id, eqtt to assert, assert wf, iff transitivity, eq id wf, int seg wf, decidable int equal, Rframe wf, decl-type wf, fpf-cap-single1, btrue wf, locl wf, Reffect wf, Rinit wf, bool wf, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, bnot wf, Id wf, fpf-single wf, Rpre wf, R-feasible-Rlist

origin